Inference at * 2 1 1 1 1 
Iof proof for Lemma member nth tl:

.....upcase..... NILNIL

1. T : Type
2. n : 
3. 0 < n
4. x:T, L:(T List). (x  nth_tl(n - 1;L))  (x  L)
5. T
6. T List
7. n1 : 
8. 0 < n1
9. nth_tl(n1 - 1;[]) = []
  nth_tl(n1;[]) = [] 

latex

 by ((RecUnfold `nth_tl` 0) 
CollapseTHEN ((((if (0) =0 then SplitOnConclITE else SplitOnHypITE (0
C))) 
CollapseTHEN (Auto)))) 

latex

C1: .....falsecase..... NILNIL

C1: 10. 0 < n1
C1:   nth_tl(n1 - 1;tl([])) = []
C.

Definitions	left + right, Unit, p q, p  q, p  q, [d], a < b, x f y, f(a), a < b, null(as), x =a y, (i = j), A, P  Q, T, P  Q, P & Q, x:A  B(x), P  Q, tt, A  B, True, t  T, b, b, i <z j, , i z j, ff, , tl(l), nth_tl(n;as), n - m, #$n, [], x:A. B(x), x:AB(x), a < b, , Type, s = t, type List
Lemmas	eqtt to assert, assert of le int, iff transitivity, eqff to assert, iff wf, rev implies wf, true wf, squash wf, bnot of le int, assert of lt int, le int wf, le wf, bool wf, lt int wf, assert wf, bnot wf